w:World, e:E. first(e)  (t:. time(pred(e))+1t  t<time(e)  isnull(a(loc(e);t))) 

latex

Definitions	t  T, Unit, Type, x:A. B(x), E, isl(x), b, b, A, P  Q, False, AB, , {x:A| B(x) }, , x:AB(x), outl(x), time(e), n+m, a<b, Prop, -n, Void, x:AB(x), Id, S  T, w-pred(w;e), , s = t, a(i;t), isnull(a), P & Q, P  Q, left+right, inl(x), if b t else f fi, false, i=j, , inr(x), True, pred(e), first(e), World, x.A(x), ij, #$n, n-m, <a,b>, P  Q, Dec(P), {T}, SQType(T), s ~ t
Lemmas	decidable assert, nat sq, decidable lt, ge wf, nat properties, pred wf, first wf, world wf, true wf, it wf, not functionality wrt iff, assert of eq int, eq int wf, ifthenelse wf, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, w-isnull wf, w-a wf, bool wf, w-pred wf, false wf, w-pred-wf2, le wf, w-time wf, outl wf, nat wf, not wf, assert wf, bnot wf, isl wf, w-E wf, unit wf